STARK recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 60.95 s - #1009

…needed it to be

`global_memory_configs` does NOT canonicalise. ✓ It hands its argument
straight to `global_memory_configs_from_init_page_data`, which is a
one-to-one map over the list — no sort, no dedup. So the AIR order IS
the list's own order and there is no second list to confuse this one
with. Four comments here claimed the opposite and reasoned from it,
including one that warned a reader against a mix-up that cannot occur.

⚠ The word still belongs somewhere, so it is moved rather than deleted:
canonicality comes from the PROVER, whose `touched_page_bases` builds
the list through a BTreeSet. On the VERIFIER's side it is a CLAIM and
does not need to be a guarantee, because it is bound twice —
`absorb_global` absorbs the list before any challenge, and a restated
set leaves the GlobalMemory bus unbalanced or the AIR count mismatched.
That is the reason the emitter can take the list as given, which is what
the old comments were groping for and got backwards.

No code moves: the emitter already indexed pages positionally and
absorbed the list as it travels, which is correct under a one-to-one
map. Only the reasoning was wrong.

The canonicality correction replaced a clause and left the rest of its
sentence dangling — "and the AIRs are / built from, which is a
different job done in a different place" — which was both broken prose
and, worse, still asserting the separation the same commit had just
disproved. There is no different job: one list is absorbed and indexes
the AIRs, which is why the emitter can take it as it travels.

…age budget

The retired rule charged every page the whole prepared chain, so two pages
worth 89,915 rows apiece were each refused and 180,036 rows were spent keeping
them sparse — more than the chain that was declined. A fixed cost charged
per page cannot be right; the fix is to charge each term to the thing that
causes it.

PART 1, per page and set-independent: a genesis page is a CANDIDATE when its
sparse leg exceeds what carrying it would ADD to the prepared leg. The
marginal is one eq with its group join, one prefix indicator per stacked
column, and one shared Sub, evaluated at a FIXED height
`num_vars + ceil(log2(2 * P_touched))` rather than at the stack's own — the
real height depends on the answer, and all three parties must reach the same
set from data they hold before deciding. On the block that is 103 rows, so
tau = 5.

PART 2, once on the whole set: the candidates' total savings must exceed
PREPARED_LEG_ROWS, which now prices the chain and nothing else. If it
refuses, every candidate stays sparse; a subset still pays the whole chain.

The block still selects 0x0, 0x40000 and 0x280000 in that order, and the
consequences are asserted with their numbers on real plans: the 27 zero pages
fail part 1 at 18 rows against 103; a lone page is carried at 9,731 entries
and left sparse at 9,730; two pages of 5,000 now share one chain; and a
fixture's 112-entry page passes part 1 and is refused by part 2, which is why
PageRoute records candidacy separately from the answer.

The sparse-leg cap's overlap test is re-derived in the same commit. Its bound
was 9,724 under the retired rule and is 9,730 under this one; both are under
the 60,000-entry cap, so a test left at the old number stays green while
measuring a rule that no longer exists. The quantity now lives with the rule
as `densest_sparse_entries`, and the cap's own refusal message cites it
instead of asking for a protocol change that has since landed.

Two readings pay for the form rather than restating it: the marginal is
differenced out of the emitter's own `weight_at_rows` across 29 and 30 pages
in one bracket, and the terms the form omits (two absorbs and two challenge
powers per page) are shown to move no boundary the rule is quoted for.

Brings V1j's gated tip cdd5d1b (eight commits over 60d7903) under the
harness stage, the root and the main sync, so the tree that composes a block
artifact runs on the emitter V1j's F1 now predicts by value.

NO CONFLICTS, and the file intersection against this branch is ZERO — verified
with a two-sided positive control, because a zero from a search is a hypothesis
until a control shows the search can return a one.

The semantic check, over V1j's whole diff since the base: no reference to
`TableCounts`, `NUM_TABLE_KINDS`, `NUM_TABLE_COUNTS`, `RowWitness` or
`FIXED_TABLE_COUNT`, and none to any statement tag or fixed-part constant. So
the three facts the main sync rests on survive by construction — V1j touches no
file that carries them, and `global_airs_for` is not in its list at all.

⛔ The zero overlap hides a real call surface and it was checked directly rather
than inferred: V1j changes `whir_global.rs`, the emitter this harness calls.
No public signature there moved; `emit_global_publishes`, `bookend_roots`,
`GlobalLayout` and the `preprocessed.is_none()` assert are untouched, so the
cross-epoch wrap's 14 published words and the root's 142 cannot move. The hunk
inside `whir_global_program` and both `GlobalRoute` hunks are comment-only —
the correction that `global_memory_configs` does NOT canonicalise, so the AIR
order IS the wire order.

What V1j did change in the emitter helpers is one pattern: count-returning forms
became value-returning ones, so the F1 predicts the interned constant pool by
value instead of by count. `emit_sumcheck_rounds` takes its two constants from a
named `newton_step_constants` instead of computing them inline;
`fold_coset_consts` returns the values it used to count. The constants are the
same constants. ⇒ every IDENTITY line is expected UNCHANGED at this tip, and a
move would mean a value-form does not reproduce the arithmetic it replaced.

Nothing is compiled here. This tip's first build is its gate.

…ormula

Part 1 charged each page a hand-written three-term form: one eq, two prefix
indicators, one shared Sub, 103 rows. Two readers then checked that form and
each found a term the other's lacked — three more per-column terms in
stacked_verify_cost outside weight_at_rows, and an absorb of three coordinates
per column into a THREADED sponge whose row cost depends on where the previous
columns left the buffer. A number two careful readings disagree about is not a
closed form, and the sponge term means no hand-written one can be exact. A
folded correction would have been worse than the understatement it fixed: still
missing that term, and now looking complete.

So the marginal is GENESIS_PAGE_MARGINAL_ROWS, a literal beside
PREPARED_LEG_ROWS, measured at MARGINAL_MEASURED_AT_VARS = 24, the height the
block's thirty genesis pages give. The three-term derivation stays as its doc,
explaining the magnitude and naming what it cannot account for. It is marked
UNPINNED and a FLOOR: the pin that turns it into a measurement lives in lfm and
belongs to the lane that owns the cost form, and nothing else may assert
equality with it. One literal is also why the three parties agree — they read
the same number rather than evaluating the same formula correctly, which is
stronger than the set-independence the fixed height bought.

Two ruled quantities move at 109 and the tests now derive rather than hard-code
them. Tau is 6, not 5: it holds at 5 only for a marginal in [90, 107], and the
only page reclassified carries five nonzero genesis bytes, which neither the
block nor any fixture does. The lone-page pair (9,730 sparse, 9,731 dense)
holds only for a marginal in [92, 109] and stands on ONE ROW at 109 — the page
just over it clears the chain by a single row — so a pin above 109 moves the
pair to (9,731, 9,732). The tests assert densest_sparse_entries() and one more,
and a band sweep states each consequence's exact band: the block's three pages
hold across [19, 2,100,474], the fixture's refusal everywhere, the two shared
pages across [1, 2,484].

The emitter test is rescoped to a LOWER BOUND. weight_at_rows is a partial view
of the cost form, so an equality against it would contradict the real pin the
day it lands. It now reads the two terms that form does account for, 102 across
one more page in one bracket, and requires the literal to be at least that plus
the amortised Sub.

…es today

The literal shipped at 109, built as the three-term reading plus the six
per-column rows the cost form pays outside weight_at_rows. Two things were
wrong with that. The 103 it was built on carried a shared Sub charged at one
per page, and that term is per-POLYNOMIAL: differenced across one more page at
one stack height it contributes ZERO, so the deterministic marginal is 102 + 6
= 108, not 109. And the threaded-sponge term is unmeasured, so 109 was 108 plus
a guess at it — wrong in an unprincipled direction.

103 is what the rule actually charges today. The literal is then a faithful
record of current behaviour, every consequence documented against it is true on
the day it lands, and it is wrong in a direction the doc states: it understates
the deterministic reading by five, which makes part 1 that much too eager until
the pin lands.

Consequences restored to their ruled values: tau is 5 again, the block's
savings 10,248,261, the fixture's 1,931, two pages of 5,000 saving 89,915 apiece
and 179,830 together. The lone-page pair is unchanged at (9,730, 9,731) — it
holds for any marginal in [92, 109], so 103 sits with six rows of headroom
rather than on the edge.

The pin's expected reading is now pre-registered as an executed table rather
than a claim: a measurement of 108 or 109 moves tau to 6 and leaves the pair
alone; 110 or more moves the pair to (9,731, 9,732). The band sweep asserts
both, so when the pin lands the consequence is already written down. The point
the retired immateriality test made is kept as one point of that sweep.

The weight-term test is renamed to say what it bounds and its doc now explains
why the difference is 102 and not 103: the shared Sub differences to zero, so
requiring the literal to be at least 102 + 1 is exactly the statement that it
contains every term that form can see.

`cargo clippy -D warnings` refuses `prepared_claims`' return type as too
complex, on the library target and on six of the nine lint steps. The type grew
when a prepared opening stopped naming one table: it gathers a point per
settled column and a value per settled column, and both are vectors of vectors.

A type alias, which is clippy's own suggestion and not an allow. It carries no
bound: a bound on a type alias is not enforced, and `FieldElement`'s own is
checked at every use — the form `sumcheck::RoundGroup` and
`batch::ResidentProof` already take in this workspace.

A pure type alias is a name for a type that already existed, so no signature,
no layout and no byte of any proof moves.

… maximum

There is no single per-page marginal. The prepared leg's sponge is threaded:
every column absorbs three coordinates into one buffer and a single squeeze
follows, costing div_ceil(4) + div_ceil(8) + 1. A page is two columns, so six
felts, which divides neither 4 nor 8. Differencing across one more page gives
s = [2, 3, 1, 3] repeating with period 4, and the marginal is 109, 110 or 111
depending on which page is added. An equality against one number is
unsatisfiable for a cost that has three.

The literal becomes the MAXIMUM of that spread. Part 1 then asks a page to
beat the dearest position it could occupy and part 2 understates its savings,
so both parts are conservative, while all three parties still read one number
which is what the single literal was for. An average would charge some pages
less than they cost.

Derived, not measured, by two independent readings that agree, and the doc says
so along with the assumption it rests on. It also says what it does not bound:
the indicator term grows two rows per prefix bit, so a stack one bracket taller
costs up to 113 a page. Raising it there would move neither consequence, since
both bands reach past it.

Two derived quantities move and the tests name them rather than hiding them.
The threshold in nonzero entries is 6, holding across a marginal of [108, 125].
The lone-page pair is (9,731, 9,732), holding across [110, 127]. The sparse-leg
cap's bound moves with it, which the ruling's list did not mention and which
would have reddened the gate. The band sweep now walks the whole spread and
shows the threshold invariant across it, so the choice of maximum over midpoint
costs exactly one entry on one quantity.

Five clippy errors that the alias commit let clippy reach, fixed as its own
suggestions and never an allow. The weight-term bound becomes a strict
inequality. The threshold's floor assertion becomes a const block, so falling
under the deterministic floor stops the tree compiling rather than failing a
test nobody ran. A manual modulo becomes is_multiple_of. A test helper's
five-tuple gets a named alias.

`genesis_stack` becomes pub(crate) rather than its return type becoming public:
that type's own field is a vector of another crate-private type, so widening
would have published two types' fields, and every caller is in this crate.

… draft

The alias commit let clippy reach the newer commits and the gate found five
errors, each fixed as clippy's own suggestion and never an allow. The weight
term's bound becomes a strict inequality. The marginal's floor assertion
becomes a const block, so breaking it stops the tree compiling rather than
failing a test nobody ran, and it now asserts the one bound that holds whatever
that number becomes: it must exceed the 102 rows the weight closure alone bills.
A manual modulo becomes is_multiple_of. A test helper's five-tuple gets a named
alias.

genesis_stack becomes pub(crate) rather than its return type becoming public.
Widening the type cascades, because its own field is a vector of another
crate-private type, so two types' fields would have become public API; every
caller is in this crate, and widening later is trivial where un-publishing is
not.

The same gate failed two assertions, and both were about a draft rather than
about the rule. A margin asserting the zero pages sit a factor of six under the
threshold was true while the marginal was 109, false at 103, and true again at
111: a margin stated as a fixed multiple of a number that moves cannot survive
that number moving. It is now the ratio it is, printed, floored at the weakest
value any candidate gives. And the threshold band was tabled as five on one
range and six above it, which is not a band; the sweep ran past the end of what
had been written down and found seven. All three sub-bands are asserted now,
with both edges.

Where the literal falls is computed rather than named. Every earlier version of
that test named the band it expected, so each time the number moved the test
reddened on the naming instead of on the finding. It asserts only that the
literal lies in the band for its own value, which holds at the current figure,
at the form that is coming, and at the higher one a taller stack costs.

The marginal's doc records why three shapes have been tried and why the
arithmetic was never the problem: a formula wrong for omitted terms, a literal
wrong because the quantity is not constant, and a formula again whose one
irreducible term is a measured bound. The value stays where it is; the form and
its measurement belong to the pin.

An `assert_eq!` message is a FORMAT STRING, so `{109, 110, 111}` in it is
read as a format argument and rustc refuses the file: "invalid format
string: python's numeric grouping ',' is not supported in rust format
strings". The test crate does not compile at 52c6cc1 or at 8a3f549
for that one line, and nothing else stands between this branch and its
merge.

`{{…}}` is rustc's own hint, and the rendered message is unchanged.

⚠ THE TRAP IS THAT THE LINE LOOKS LIKE PROSE. It sits inside a
backslash-continued string and carries no quote of its own, so a reader
scanning for string literals skips it and a search anchored on a quote
misses it. Two independent sweeps of this branch's six commits agree on
the count: over `60075209f..8a3f549`, the brace-on-a-digit class has
exactly ONE occurrence and this is it; the brace-enclosed-list class has
six raw hits, five of them inside doc comments where braces are inert,
plus this one. Both sweeps were calibrated against this known line
before being trusted, because a pattern that cannot match the one hit
you already have returns a confident zero.

The author of these commits has retired; this lands on their branch
under the lead's authorisation, and carries nothing else — the shape
change the marginal is getting belongs to the commit on the merged tip.

Brings W1j's gated tip 644b7de (eighteen commits over 60d7903) under the
harness stage, the root, the main sync and V1j's constant-pool forms. With it
the branch carries every half of the WHIR pipeline that exists: the base, the
level-0 wraps, the cross-epoch stage, the shared interior and the root.

NO CONFLICTS. The file intersection against this branch is TWO —
`continuation.rs` and `tests/multilinear_bench_tests.rs`, both moved on this
side by the main sync — and `git merge-tree --write-tree` wrote
7c4ef1c for the pair before the merge ran.
Both instruments carry their own control: the intersection was taken with a
two-sided positive control (the same search shown able to return a hit against
each list), because a search reporting nothing to merge is not evidence until
it has been shown capable of producing one.

The semantic checks, over W1j's whole diff since the base: no statement tag and
no fixed-part constant moved, and the single hit on the table-kind class is
`Error::InvalidTableCounts` — a variant whose NAME contains the string, not a
construction or a destructure. So the three facts the main sync rests on
survive: the elision still does not reach the cross-epoch AIR set, the
cross-epoch statement's tag and its 134-byte fixed part are unmoved, and
nothing in this lineage builds or destructures a `TableCounts`.

⛔ WHAT THIS MERGE BRINGS THAT THE HARNESS CANNOT YET CONSUME. W1j's
`prove_global` hands `multi_prove` a genesis opening, so a run with a genesis
stack now produces a cross-epoch proof whose `preprocessed` is `Some` — and
`whir_global_arena` still opens by asserting that it is `None`. Three sites
answer it, in one commit and not this one: drop the assert, extend the arena
with the opening's words, and teach the program to hint and verify that chain.
⚠ No fixture here reaches it. The laptop fixture's only page is the
private-input one, which carries no genesis, so the arm stays green while the
block — thirty of thirty-five pages on OFFSET+INIT — would fail at the global
stage. The dense-genesis arm written for that commit is what closes the gap.

The asm guest count goes 220 to 221, so the gate's ELF expectation is 266, and
it is a recorded check rather than a printed number: a 265 after this merge is
exactly the symptom of the new guest failing to build.

Nothing is compiled here. This tip's first build is its gate.

…acket, and the cross-epoch program emits the prepared opening

PART 1's term stops being a literal. `marginal_stacked_rows(num_vars,
n_fixed)` is the rows one more carried page adds to the prepared leg,
evaluated at the height THIS run's genesis page count puts the stack at:
101 at a lone page's bracket, 111 at the block's, 113 one bracket up.

Three shapes were tried and the arithmetic was never the problem. A
FORMULA, wrong because it omitted terms — two careful readings each found
a term the other's lacked. A LITERAL, wrong because the quantity is not
constant: it takes three values at one bracket and three more one bracket
up, and a literal carries its bracket only in prose, where prose goes
stale. A FORMULA again, whose one irreducible term is a proven BOUND.
⇒ when a cost splits into a deterministic part and a bounded
nondeterministic one, write BOTH: a literal hides the split, and a form
that omits the bound looks complete while being wrong.

`MAX_SPONGE_MARGINAL = 3` is that bound, proven rather than measured: the
wrapper absorbs three coordinates per column into one threaded buffer and
squeezes once, a page is two columns, and six felts move `ceil(f/4)` by 1
or 2 and `ceil(f/8)` by 0 or 1.

SET-INDEPENDENCE SURVIVES, which is what the single literal protected.
`n_fixed` is `fixed_stack_vars` of the GENESIS PAGE COUNT — a quantity
prover, verifier and emitter each derive from the ELF and the touched page
list before any routing decision exists. It is never `n_dense`, which is
the rule's own output.

TWO DOCUMENTED CONSEQUENCES MOVE, and both are the form following the run.
A lone page is charged at its own bracket, so its boundary is (9,730
sparse, 9,731 dense) with nine rows of margin over the chain, while a page
inside the block's thirty faces (9,731, 9,732); both are asserted, each
naming its bracket. And τ is not invariant across brackets — 5 while the
marginal is under 108 and 6 from there, crossing at nine genesis pages —
so the band sweep walks the brackets and asserts exactly one crossing.
⚠ Every such figure here is PREDICTED from the source, not measured: the
box reads them at this tip.

THE PIN, `whir_stacked_tests::the_marginal_the_routing_rule_charges_is_
the_one_the_stack_bills`, is where the form meets the cost form. It walks
both single-polynomial brackets, guards each page count (one polynomial,
the expected height), differences `stacked_verify_cost` across one more
page, and asserts the form equals the DEAREST page the stack bills, the
sponge term inside its bound at every position and the bound reached, and
τ invariant across the spread. It also walks the same brackets under a
different blowup, folding, security level and grind and asserts the
marginals are identical — the claim that every chain term is
per-polynomial, executed rather than argued. It needs no hash posture: it
proves nothing and harvests nothing.

THE CROSS-EPOCH PROGRAM NOW EMITS THE PREPARED OPENING, which is the half
of the hybrid the emitter owes. The stack's roots are interned and
absorbed in the roots block where `absorb_roots_and_challenge` puts them;
the opening's chains are hinted after every group's; and the leg is
`emit_stacked_verify` over one point per column, each page's own columns
gathered at that page's own reduced point — the same gather
`prepared_claims` performs, so the opening proves the pinned commitment
takes exactly the values those tables settled on, with no separate
equality anybody has to remember to write.

⛔ THE DENSE SET IS READ OFF THE OPENING, NEVER RE-DECIDED. Re-running the
threshold in the emitter is the one way this leg goes silently unsound: a
program could then skip a `check_preprocessed` the opening does not cover.
`GlobalPlan::build` reads `GlobalPrepared.at` and refuses any shape it
cannot mirror — a run that is not a genesis page's whole preprocessed
prefix, a table visited twice or out of stack order, a settled table the
route table calls a bookend or a private page.

⛔⛔ AND EVERY PREPROCESSED COLUMN IS COVERED EXACTLY ONCE — settled by the
stack XOR checked by a closed form — asserted by a pass OUTSIDE the match
that produces the routing. Written inside it, the check would restate its
own expression and could not fail. The failure it exists for is a page
that falls between the two routes: no value is wrong, the program is
merely shorter, and every value gate stays green because there is simply
no check.

The F1 gains the prepared leg and its constants, and its body becomes a
helper so the DENSE bundle gets the same comparison — without it the three
forms the prepared path adds would be written and never read, which is the
shape of defect that left seventeen tests green over a deleted
preprocessed leg.

Also here: W1h's dense-genesis arm, the only fixture that reaches the
opening at all, with an anti-vacuity check on the state it exists to
reach; the guest comment rewritten around the two-part rule, naming the
tree it was read at; and the cross-epoch driver's module header, which
said the proof carries no prepared opening and went stale because of this
change.

The sparse path is unmoved by construction: every new cost term is zero
when the proof carries no opening, which is every fixture but
`dense_data_page_touch`.

`a_candidate_the_chain_cannot_be_paid_for_stays_sparse` asserted the same
quantity twice: once derived, `plan.savings == 2_034 - BLOCK_MARGINAL`,
and once as the bare literal `1_931`. The form charges 111 where the
retired literal charged 103, so the derived side moved to 1,923 and the
bare one did not. Gate-2 read `left: 1923 / right: 1931`.

⛔ THE LITERAL NAMED NO SYMBOL, WHICH IS WHY IT SURVIVED. Re-pointing the
rule at the form was done by sweeping for `GENESIS_PAGE_MARGINAL_ROWS` and
`MARGINAL_MEASURED_AT_VARS`, and this line mentions neither: it is
`2034 - 103` with the subtraction already done. A symbol sweep cannot see
a number that has been folded, and that is the lesson worth keeping —
after the sweep, sweep again BY VALUE, recomputing each candidate from the
new form.

That second sweep is now run and recorded: over `continuation.rs`,
`whir_chain_tests.rs`, `tests/multilinear_continuation_tests.rs` and
`lfm/preprocessed.rs`, every quantity the retired 103 could have produced
was recomputed under the form and searched for in all three spellings
(plain, Rust underscores, prose commas). The 112-entry savings is the ONLY
stale one, in this assertion and in the doc sentence above it. The
5,000-entry savings, the block's savings, the 65,652 savings and the
densest-sparse bound are clean — they were re-pointed with the rule. Every
hit on 9,730 is the LONE page's pair, which the form leaves where it was.

⇒ THE FIX IS ONE DERIVATION WITH THE VALUE IN THE MESSAGE, not a corrected
literal. A number a reader wants is a message; a second assertion of the
same quantity is a thing that drifts, and drifts silently until the day
the first one moves.

The doc sentence above the test paired a 111-row marginal with a 1,931-row
saving, which could not both be true; it reads 1,923 now.

`the_block_bundle_builds_its_cross_epoch_program` built the cross-epoch
program at the block's shape and printed its size, but nothing in its
output said WHICH ROUTE the genesis took — the reading the hybrid's
ruling is actually quoted by. A box run could only infer it from the
instruction count: sparse-only would be over 10 M in INIT alone and the
emit-time cap would have refused the build outright, so a number inside
the ruled band implied the stack had been taken. An inference from an
absence is not a reading.

The line now carries `prepared <rows> over <n> dense pages at n_stack
<vars>`. Nonzero rows mean the opening was taken; zero means every
genesis page went to the closed form, which is every fixture but
`dense_data_page_touch`.

⚠ READ OFF THE DRIVER'S OWN RECORD, NEVER RE-DERIVED. The page count and
the stack height come from `WhirRealGlobal::prepared`, which is what the
VERIFICATION consumed. Evaluating the threshold a second time here would
be a second opinion about a decision already made, and the two could
disagree with nothing in the output to say which one was the run's.

A println in an `#[ignore]`d box arm: no program text moves, no proof
moves, and no fixture-scale gate can see it.

`two_pages_worth_less_than_the_chain_apiece_share_one` held
`assert_eq!(plan.savings, 179_830)` one line under the derived
`assert_eq!(plan.savings, 2 * alone)`. 179,830 is 2 × 89,915 — the
retired constant's `alone` DOUBLED — so re-pointing `alone` to 89,907
left its double behind and the box read `left: 179814 / right: 179830`.

⛔ THE CLASS IS THE SAME AS THE REFUSED CANDIDATE'S AND THE SWEEP THAT
CAUGHT THAT ONE COULD NOT SEE THIS ONE. That sweep recomputed every BASE
quantity the retired 103 could produce and searched for its stale value.
A MULTIPLE of a base quantity is a different number: 89,915 appears
nowhere here, 179,830 does. ⇒ after a form moves, sweep its SUMS AND
PRODUCTS too, not only its terms.

The extended sweep is now run — every base quantity times one through
four, and every pair-sum, in three spellings, over the four files that
name the rule — and this is the ONLY further hit. Two families were
checked rather than assumed: the lone page's boundary reads 9,730 in
several places and is CORRECT, because at that bracket the form charges
101 and the pair genuinely is (9,730, 9,731); and 180,036 = 2 × 90,018 is
two SPARSE LEGS with no marginal term in it, so it does not move at any
value of the form and stays as the retired rule's contrast.

The fix is the same shape as the first: the literal goes, and the sum
rides in the surviving assertion's message beside the per-page figure it
is twice.

…ready named it

The WHIR base prints one number for fifteen epochs - 57% of the block's
wall with nothing under it - and there is not a timer, span or print
between `multilinear_continuation::prove_continuation` and the bottom of
the chain. Every optimisation round so far has moved that number without
anyone being able to say which part of it moved.

The knob is not new. The LFM tree launcher has exported
`LAMBDA_VM_BASE_SPLIT=1` on the WHIR arm since that arm existed, 'byte
identical to the D-S exports', and it reached nothing: the WHIR base does
not go through `continuation::prove_continuation`, where the STARK
instrument lives. An inert knob printed as if it mattered is worse than a
missing one, because the export is the evidence a reader uses to believe
the breakdown was taken. The same name now means the same thing on both
pipelines, in the same line format.

The stages partition their own thread's wall: execute/collect/build/
handoff on the producer, prep/absorb/commit/prove on the prover, and
challenge/argue/open_groups/open_prepared inside the argument. The two
threads run concurrently, so their sums must never be added - what the
pair says is which of them set the wall, and `handoff` is the one stage
that can answer it, being a blocking send on an unbuffered channel.

`check_closure` is a pure function over the records, so the arms can be
fed manufactured omissions rather than only whatever a real run produces:
a missing prover stage reddens arm A naming the epoch, a missing inner
slot reddens arm B (the four stages still close without it), a missing
producer stage reddens arm C, and a zeroed tolerance reddens a run
carrying real timer cost. It deliberately does not assert that the two
sums equal the base wall; that identity is false on a correct instrument
and a check that reddens honestly gets widened until it cannot fail.

Cost when off: `mark` returns None and no clock is read.

Two defects the wiring itself surfaced. `prove_epoch` receives `label`,
not the epoch index, and `epoch_label(i) = i + 1` - keying the prover
records on it would have joined the producer's epoch 0 to the prover's
epoch 1 across the whole table. And a committed table carries no name, so
the argument can only see an index; the names are sent down from the layer
that holds the AIRs.

…ly the production one

The read-back landed in the production WHIR tree arm's base window, which
is the arm that needs a block ELF, a census and a card. The gate that is
supposed to prove the instrument closes cannot afford that arm, and ran
the production one by name: it refused in 0.00s with its own guard -
'LFM_CENSUS_ELF must name a file: this composes the PRODUCTION WHIR tree,
and a silent fixture fallback would report a fixture number under a
production name' - which is the harness being right and the gate being
wrong. An instrument checked only in the arm nothing can afford is an
instrument nothing gates.

The fixture arm keeps its own base window, so this is the same call in
the second place rather than a shared helper growing a caller.

The base wall is taken where the base ends, not recomputed lower down:
`t_all` runs for the whole tree, so a second `elapsed()` would hand the
split a denominator including level 0 and the interior, and every stage's
share would read far too small.

…n it

`open_groups` is 43.8% of the WHIR base and 24.9% of the block's whole
wall, and wt12 printed it as one number. These six resolve the round
loop: the three 20-bit grinds, the opening sumcheck, the fold, the fresh
successor commit, the out-of-domain block, and the query openings that
rebuild the tree on device per batch.

Six and not the four the round obviously has: `factors.rounds` and the
out-of-domain block are neither grind nor fold nor commit nor query, and
leaving them out would have made the closure arm redden on a correct
instrument - which is how a tolerance gets widened until it cannot fail.

Arm E asserts the six close `open_groups` per record, and it caught two
real defects in this instrument before either reached a block run.

The first: the slots are process-global, and reading them at the window's
close alone attributes to this group loop whatever ran the chain earlier
in the process. They are now cleared at the window's OPEN, so 'the group
openings only' is a property of the window and not an assumption about
callers.

The second: the out-of-domain window spanned its own grind, and the grind
was separately added to GRIND - so that time was counted twice and the six
summed to MORE than the wall containing them. Slots that partition must
not nest; the two out-of-domain windows now abut the grind instead. The
fix is visible in the slot that moved: ood 3.83s -> 0.04s.

A negative remainder is therefore not drift. It means the parts are not
parts, and it has two causes - a window that is too wide, and windows that
overlap. The message says so rather than reporting a percentage.

The prepared opening keeps its wall and no breakdown: it is 2.5% of the
base, and six more fields would not move a ranking. The success line names
arms A-E, because a line that under-names what it checked reads exactly
like a check that never ran.

…e posture in the pin's identity

Runs lb17 and lb18 measured the transcript pins at two tips of this lineage and
read the same four deltas at both: +77 absorbs, +200 squeezes and +17 states on
BOTH sides, and one device commit the model did not account for. The pins had
not actually been measured on this lineage since V3's tip -- the "unmoved"
readings from W1h's v4/v5 gate were greps matching the tuples the two
should_panic tests print, which appear on any machine and touch no guest -- so
the move is the lineage's, not any one commit's. An A/B across the two tips read
identical counters, which is what says so.

Two causes, both now derived rather than re-measured.

THE POSTURE. The constants were taken with LAMBDA_VM_MAX_ROWS_LOG2 unset, where
MaxRowsConfig::default returns the production per-table caps and an epoch
carries 34 tables; every run of record is at the uniform 2^21, where the same
block's epoch carries 27. pin_applies took the sha, the length and the epoch
size, so a run at a posture nobody pinned was the pinned configuration by the
pin's own identity. The cap is now part of that identity, read through
max_rows_log2_override -- extracted out of MaxRowsConfig::default so the posture
the pin checks is by construction the posture the epochs were chunked at -- and
the bases are the record posture's, measured at 892c7d1. A run at any other
cap skips and names both caps; another posture is not a defect, it is a
different measurement. This held on the ladder branch only; this commit is what
makes it true on this lineage.

THE STACK. The stacked INIT polynomial of the dense genesis pages entered the
cross-epoch statement after the pin's constants were taken. Its cost is now a
function of the plan the run used -- read through the verifier's own
global_airs_for(..).genesis_stack(), so no threshold is re-decided here -- and
of the chain config that proof argues at:

  absorbs   one root per stacked polynomial in the cross-epoch roots block,
            one claimed value per stacked column, then the chain
  squeezes  the batching challenge, then the chain's own draws
  states    3R - 1: three grinds a round, with no out-of-domain one on the last

At the block's six columns of 2^18 -- one stacked polynomial at n_stack 21, six
rounds at fold width four -- that is 1 + 6 + 70 = 77, 1 + 199 = 200 and 17,
which are the measured deltas exactly. A run with no dense page adds nothing,
and the unit pin evaluates the same form at n_stack 19 as well so a wrong term
cannot be flat across both shapes.

The stack costs the run once and not once per epoch, and it moves both sides
equally: it lives in the cross-epoch proof, which has no `owed` replay, so
unlike DECODE's derived root it is absorbed once on each side and owed is
unmoved. The measurement confirms that at 160 = 145 + 15 absorbs and 30 = 2 x 15
squeezes.

THE DEVICE COMMIT. commits() walked a flat list of proofs, so the stack's five
fold commits were picked up the moment it landed while its held commitment was
not: the held term was a find_map, which stops at the first proof carrying a
prepared opening, and the epoch proofs come first in the list the bench builds.
The two held commitments have different scopes -- DECODE's is a function of the
ELF and is held across every epoch, the stack's is built once per prove_global
call and belongs to that one proof -- so they are now two arguments and two
terms, and neither can be inferred from slice order. 1106 + 80 + 2 = 1188, which
is the counter's reading.

The carried bases compose with the derived terms onto the lb17/lb18 measurement
on all six numbers with no residue, which is what makes carrying them a verified
move rather than a new literal; the arithmetic is written out in the doc
comment. owed's carried half is no longer only a constant either: it is checked
against the run's own proofs -- the sum of roots.len() over the bundle's fifteen
epochs, one root per chain -- so a posture that moves the chain count reddens by
name instead of arriving as "the counts moved".

Also: make lint gains a TENTH step. Everything under cfg(all(cuda,
hash-metrics)) -- check_device_pins and transcript_pin::commits, which is the
whole device-commit model -- was compiled by no pass in the matrix: the cuda
pass carries no hash-metrics and both hash-metrics passes carry no cuda, so a
box run was that code's first compiler. From this sha the lineage's lint is ten
steps run separately, not nine, and the tenth needs no GPU.

… lint step needs the parity allow

Two fixes to the commit before this one, both found by running the gate rather
than by reading it.

then_some. `global_stack` built its Option with `.then(|| StackShape { .. })` on
a struct literal with no side effects, which `clippy::unnecessary_lazy_evaluations`
rejects under -D warnings. Lint step 9 caught it; the commit before this one had
been made with that step red, because the gate script committed unconditionally
between the test run and the mutations. The script now refuses to commit while
any step above it is red -- a script that commits on a red is the same class of
defect as a gate whose verdict is not read.

The tenth lint step. It was added without `-A clippy::op_ref`, which every one
of the other nine carries; without it the step reports 156 op_ref errors from
code the workspace writes that way by design, so it was a step that could not go
green on any sha. The line is now

  cargo clippy -p lambda-vm-prover --all-targets --features cuda,hash-metrics -- -D warnings -A clippy::op_ref

and with it the step reads exit 0 with zero error lines, which is what makes the
device pin's cfg(all(cuda, hash-metrics)) code covered rather than merely
mentioned. From this sha the lineage's lint is ten steps run separately.

One finding recorded and NOT fixed here, because it is outside this lane: a
clippy pass with --all-features -- a posture the Makefile's matrix never runs --
fails on crypto/stark/src/prover.rs:1544, `too_many_arguments` (8/7) on
`commit_main_trace`. Nothing in this branch touches that file.

The six chain slots closed to +1.4% on the laptop and +5.1% on the box's
card-free fixture. Widening the tolerance to admit 5% would have made the
arm unable to fail, and it would have been wrong about the cause.

The cause is not the round loop's bookkeeping. `Factors::from_shares` runs
in `prove_shared`, and `stacked_eval::prove` builds the weights and the
stacked polys, all inside `open_groups` and outside the round loop
entirely; `config.schedule` and `domain.clone()` sit before the first
round. That is a setup phase - the same class of miss as the
out-of-domain grind - and it is roughly fixed per epoch, so its share
grows as the window shrinks on a faster machine.

So the loop's own wall is measured, and what was one unattributed gap
becomes two NAMED terms: `round_other` is the loop's bookkeeping between
windows, `setup_tail` is everything outside the loop. The reading says
which owns the gap rather than a comment asserting it. On the fixture it
is unambiguous: round_other 0.00 on every record, setup_tail 0.20 / 0.17
/ 0.16 / 0.01.

Arm E had to change with it. `Sigma(six) + round_other + setup_tail =
open_groups` is an IDENTITY once the wall is measured - the remainders are
defined as the differences - so asserting it would be a check that cannot
fail. It now asserts what can: both remainders NON-NEGATIVE. A negative
one is not drift; it means the parts are not parts, and the two bounds
separate the two causes - the six overlapping or escaping the loop, and
the loop escaping the opening. Those are the shapes the two real defects
took.

A slot merely reading small is therefore a READING, not an error: its
time lands in a named remainder. One unit case exists to assert the arm
does NOT redden there, so it cannot drift back into asserting an
identity.

The seventh slot fixed a false red and removed the check's power to see
a missing timer. Asserting only that the two remainders are non-negative
meant an omitted slot shrank Sigma(six), so round_other = round_wall -
Sigma(six) GREW - positive, allowed, invisible. The gate proved it: the
mutation arm E caught before the round wall existed sailed straight
through after it.

The identity was never the thing to remove; ASSERTING the identity was.
round_other is the loop's own bookkeeping and reads 0.00 on every record
of a correct instrument, so an upper bound at 3% of the loop's wall is
enormous headroom honestly and trips on any omitted slot above it.
setup_tail keeps >= 0 only: it is legitimately un-slotted work outside
the loop, and bounding it would assert a size nobody measured.

Two more defects surfaced while fixing it, both from the unit run rather
than from reasoning.

The honest() fixture carried a 5.9% remainder and tripped the very bound
it was written to test. A fixture that is not itself a correct instrument
makes every arm built on it meaningless, so the wall now models what real
records show: Sigma(six) plus a hair.

And the checks ran in the wrong order. A loop wall that escapes its
opening also leaves a large positive round_other, so with the accounting
check first it was reported as 'a slot is not being added' - the wrong
defect, named confidently. Containment is checked before arithmetic.

The new unit case has a twin that must NOT redden: a slot genuinely
small, where the wall shrinks with it. Without it, queries reading 0.00
on any card-free fixture would become a permanent red and the next lane
would widen the bound to silence it.

…ck, the cap in the pin's identity, the tenth lint step

…t it is not

`LAMBDA_VM_GRIND_SCAN_FACTOR` (default 8 — the record posture, unmoved)
replaces the literal 8 at the one site that sizes a device grind's launch
block. Read once per process through a `OnceLock`, refused outside 1..=64 with
the offending value named, and printed as `★ GRIND SCAN FACTOR: n` on the
first device grind, so a log that quotes the factor can be shown to have read
it rather than assumed it.

⛔ The knob is NOT the lever it was ruled to be, and the doc comment now says
why. Both grind kernels carry `if (nonce >= *result) break;` against a
`volatile` result the `atomicMin` writes through L2, and the stride walk gives
every nonce in `[base, base+count)` exactly one owner — so the scan stops at
the first hit. The permutations executed are `h + stride` whatever the block
size, and the launches before the hitting one cover exactly the part of
`[0, h)` below it. The factor buys only the probability that one launch
suffices, `1 - e^-k`. Lowering it removes no permutations (they were never
executed) and adds `1/(1 - e^-k)` expected round trips.

The same reading says the returned nonce is the globally smallest valid one at
any factor — which `tests/grinding.rs::gpu_grind_returns_smallest_valid_nonce`
already pins — so sweeping the knob moves no proof byte.

`prover/tests/rpx_grind_bench.rs` is the arm that settles this on the card in
seconds rather than in four tree runs: ms/grind and the full nonce list at one
scan factor per process. Flat means the block is a ceiling; halving means the
scan dominates; an identical nonce list across the arms is the byte control.

…ead off the driver

`LAMBDA_VM_GRIND_GRID` joins `LAMBDA_VM_GRIND_SCAN_FACTOR` in one module, both
read once, both defaulting to today's exact values (8 and 1024) so the record
posture is byte-unchanged. ONE line prints both AND the stride each arm gets —
`★ GRIND KNOBS: scan 8 · grid 1024 · stride rpx 131072 / keccak 262144` — because
the stride is the mechanism and a reader should not have to multiply it back
out. The two block dims stay constants: they are tuned per kernel against
register pressure, which belongs to the kernel body, and moving them would
change what an occupancy reading means.

Why the GRID is the candidate lever now that the scan factor is not. The
kernels stop at the first hit, so a search executes `h + stride` permutations
and `stride = grid × block_dim` is the term left behind — the overshoot is
`stride/h`, 12.5% at the default. That gives the knob two opposite edges: while
the card is not filled a wider grid raises throughput faster than overshoot,
and once it is filled the surplus blocks only queue and the wider stride is
pure added work. The sweep therefore has to run BOTH ways.

`device_fill()` answers which edge the default sits on by READING the driver —
SM count, max threads per SM, the kernel's registers per thread, and the
occupancy the driver will actually grant — instead of estimating residency from
a block dim. A grid above the resident-block ceiling buys no parallelism.

`search` now takes its knobs as a parameter, so `generate_nonce_{gpu,rpx_gpu}_at`
can sweep them inside ONE process. That is not a convenience: the knobs cache in
a `OnceLock`, so comparing settings through the environment would need a process
per arm, and four processes are four device contexts, four cubin loads and four
clock domains compared across an exponential spread of hit distances. Paired
arms on identical seeds make the ratios exact instead.

`prover/tests/rpx_grind_bench.rs` runs the nine arms that way — scan 8/4/2/1 at
grid 1024 and grid 256/512/1024/2048/4096 at scan 8, the 8/1024 arm shared — over
256 seeds at the production factor, reporting mean, median and `ns/perm`. The
nonce IS the hit distance, so the permutations a launch executed are known
exactly and `ns/perm` is the seed-independent throughput the grid question turns
on. Three controls travel with it: the environment path is exercised and
asserted to agree with the explicit one, every arm's nonce list must be
identical, and the measured ms/grind is projected over the base's 3,428 grinds
against the window wt14 read (15.73-18.03 s) and reported in or out.

`crypto/math-cuda/tests/grinding.rs` gains the card-side twin: the nonce is the
same, and still the smallest, at every scan factor and every grid.

…anism

The first run read a monotone fall down the scan column — ratios of 1.000,
0.953, 0.872 and 0.800 at scan factors 8, 4, 2 and 1 — which the kernels say
cannot exist. Both stop at the first hit, so the executed permutations are
`h + stride` whatever the block size, and for the median seed, whose hit falls
inside even the narrowest block here, the two launches are the same kernel
doing the same rounds. There is nothing for the knob to change.

The arms ran in one fixed order in one process, so that fall is confounded with
drift. Pairing on seeds cancels the seed spread; it does not cancel a boosting
clock. Four changes to the procedure, none to the measurement:

Every seed now runs every arm in a rotating order, so each arm sits in every
position of the rotation equally often and drift pairs out too. The control is
repeated as a final arm with identical knobs: its ratio is the noise floor,
measured rather than assumed, and no arm may claim less than it. Statistics are
per-seed and paired — the median of the per-seed ratios and the count of seeds
the arm actually beat, because a real twenty percent shows on most of 256 seeds
while drift shows as a trend a rotation destroys. And the combined arms run, in
case the two effects are real and additive.

★ The split that can falsify a mechanism. The returned nonce IS the hit
distance, so every seed can be labelled by whether its hit fell inside the
arm's block. Seeds inside take one launch and run the identical kernel at every
arm, so no knob can touch them; seeds outside are the only ones that miss and
relaunch. An arm whose gain is the same on both groups is not the knob, it is
the procedure. A gain living only in the outside group is a real miss-path
effect and owes a mechanism from the kernel before it is priced.

… survives a zero

QUERIES is the largest slot in the WHIR chain and, like `open_groups` before
it, one number. Four slots partition it — `QUERY_SAMPLE`, `TREE_REBUILD`,
`COSET_GATHER`, `OPEN_ASSEMBLE` — counted on EVERY `open_many` call, which is
twice per non-final round because `whir_round::prove` opens the current
commitment and its successor, and once in the final round.

⛔ The boundary is `open_many`, not `paths()`. On the device arm `paths()` is a
range check, ONE device call and a `map` into `Proof`, so splitting inside it
would weigh the rebuild against host bookkeeping over a hundred kilobyte-sized
paths and read ~100% every time. What competes with the rebuild is the coset
gather, which sits beside `paths()` rather than inside it and would otherwise
stay in QUERIES as an unnamed remainder — the same shape as the setup gap the
seventh slot was added to name.

`queries_other` is bounded above as well as below, and the bound carries an
ABSOLUTE allowance beside the relative one. Card-free the fixture's query
openings read 0.00 s, and three percent of two milliseconds is below the glue
between the windows and below the clock itself, so a purely relative bound
would fire on the honest path at the shape the gate actually runs.

★ Arm F is the arm that survives that shape: `rebuild_calls` must equal
`2·round_count − chain_count`, every term counted by the run rather than read
off the source. The durations vanish card-free; the calls do not.

⛔ And the term is CHAINS, not groups. `stacked_eval::prove` runs one chain per
COMMITMENT in the stacked commitment, so a group can open several, and an
identity written over groups would have been red on the honest path the first
time one did. Its guard is "any of the three counters is nonzero" rather than
"the rounds are", because guarding on the rounds alone makes a dropped ROUND
counter invisible — the same blind spot the seventh slot opened in arm E.

The harness sums the four over the epoch records and prints `tree_rebuild`'s
SHARE of the query openings, which is round 3's kill condition: retention
removes the rebuilds and nothing else, so if they are not the bulk of QUERIES
the lever is dead before any lifetime code is written.

The closure line now names arms A-F, because a line that under-names what it
checked reads exactly like a check that never ran.

★ The new arm found a defect in the existing fixture on its first run: the
"must NOT redden" twin zeroed the QUERIES slot while leaving the four inside it
at their honest values, which models four parts summing to more than their
whole. The fixture was wrong, not the bound.

…es the mean

⛔ The launcher read the repeated control's ratio by COLUMN POSITION, and that
arm's label is two words, so it read the throughput column instead. It reported
the procedure as 327% unstable on a run whose ratio column read 1.000 — a check
that could not pass, in a script that reads every other verdict by name.

The fix is not a better column index. The bench now prints the floor on its own
named line, so nothing downstream has to count spaces to find the truth.

And two readings the means still owe. The per-seed median ratios are flat while
the means fall, which is a statement about a distribution, so the distribution
is now printed: the deciles of the per-seed ratio per arm, and the twenty seeds
that move the mean most against the control.

Each of those twenty carries its hit distance and its launch count at both
arms. The launch count is DERIVED rather than instrumented — the search
advances its base by one block per miss and returns on the block containing the
hit, so the count is the hit distance over the block plus one, exactly. It is
the only quantity that differs between two arms for one seed, which makes it
the discriminator: if the twenty are the largest-hit-distance seeds and their
launch counts exceed one, the effect lives in the miss-and-relaunch path or in
what a long sustained launch costs under the board power limiter, and the card
drew its full power on that run. If they are ordinary seeds, neither survives.

…nd is the only thing left

v4's top-20 killed three of the four candidates for the tail effect. The seeds
that move the mean are SMALL-h (258k-512k, inside 2^20), take ONE launch at both
arms, and it is the CONTROL that is slow by 5-11 ms while scan 1 costs what
`h + stride` predicts. That rules out the power limiter (these are not the long
sustained launches), the miss-and-relaunch path (one launch either way) and the
volatile load's per-iteration cost (the same iterations either way).

What is left is readable from the code. For a one-launch seed `search` does
nothing that scales with `count` — one 8-byte sentinel, a launch at a grid the
knob fixes, 8 bytes back, a synchronize — and inside the kernel `count` reaches
exactly one thing, the loop bound `i < count`. Work is `h + stride` ONLY IF the
early exit stops every thread; a thread that never observes the atomicMin runs
to `count` and wastes in proportion to it.

So sweep the knob UP instead of down. Scan 16, 32 and 64 join the arms, and the
new COUNT SLOPE section prints each arm's excess over the tightest cap in the
sweep, normalised to the control, BESIDE its prediction (k-1)/7. Count-bound
reads 2.14 / 4.43 / 9.00 at k = 16 / 32 / 64; saturated reads ~1.00 from k = 8
up. The two branches are a factor of eight apart at k = 64, which no clock ramp,
thermal drift, ordering or seed spread produces.

The grid pair is run at BOTH caps (grid 4096 at scan 8 and at scan 1) so the
same defect can be tested from the block-count side: if wide grids make
stragglers worse by contending the atomicMin's line, a tight `count` should mask
it. Equal damage at both caps refuses that unification.

The verdict is printed on a named line and the section is read by its name, not
by column position or section order: `scan 64` also begins a row in THE ARMS and
in the DECILE tables, so the launcher anchors the read to the COUNT SLOPE
section itself. That is v3's lesson, which cost this file a noise floor that
could not pass.

No default moves. Scan 16/32/64 exist to make waste visible by exaggerating it
and are candidates for nothing; the record posture stays scan 8 / grid 1024.
This measures wasted work, never a wrong answer: the nonce control asserts all
twelve arms return identical nonce lists before any timing is read.

…evice halves

The artifact build (`build_artifacts_with_hasher`) now walks its commits
through `lfm::artifact_walk`: one plan (the eleven slot groups, the
LFM_BLAKE3 chunks, the LFM_HASH tail, under row-pair and, when the format
has it, one-row leaves) and one walk parameterized by a pass. `Pass::All`
is the build exactly as it ran: the same windows of `groups_in_flight`,
the same just-in-time BLAKE3 chunk materialization, the same
`commit_group_device_or_host_with` per group.

New, and unused by any caller yet: `build_artifacts_with_device_section`
(and `build_artifacts_sectioned`, which also returns the split). It walks
`Pass::Host` first — the groups the device would decline, committed by
`commit_group_host_with`, which cannot reach the card — and then enters a
caller-supplied section (a card permit) for `Pass::Device`, in the same
windows minus the host groups. The merge refuses a slot committed on both
sides or on neither. Routing is `gpu_lde::commit_reaches_device`, the
admission `admit_commit` applies (no device or below the row floor
declines; over budget still reaches the device and aborts there).

The registry drift tests pin the default walk's roots; the merge's two
refusals are unit-tested.

…t field

A WHIR round has three proof-of-work slots (folding, out-of-domain, query),
and the proof carries three nonces a round whatever the bits. A slot whose
grind has zero bits, and the last round's out-of-domain slot, is carried and
never read, so any value in it verifies. A query-only grind (P2) would leave
two such unbound fields a round.

ChainFormat gains `nonces: NonceLayout`:
- Three (the default): today's format, byte for byte.
- Spent: a round carries only the nonces its grinds spend. The in-guest
  arena has no word for an unspent nonce; ChainShape::carries is the one
  place the layout is written, and the word count, the hints and the arena
  words all read it. The host verifier refuses a nonzero value in a host
  field the layout does not carry (Error::UnspentNonce). RoundNonces keeps
  its three fields, so both layouts share one proof type and Three keeps its
  bytes.

GrindBits::query_only(bits) grinds before the query positions only. The
query count reads the query grind alone, so it does not move.

No production config uses Spent or a query-only grind yet, so every proof,
program and pin is unchanged. The legacy layout's chain programs, arenas and
proof bytes are pinned against values printed at 0428c39, and the
transcript closed form now prices only the grinds a config spends.

…t off)

STARK level 0 idles the card 12.9 s of 79.3 s (G1): 5.44 s inside
build_artifacts holds (64 % idle), 4.95 s inside multi_prove holds (30 %),
2.85 s with no hold. The interior's holds, on larger programs, are 10 % and
13 % idle; what differs at level 0 is the host load of the other five
workers (the epoch reconstructs above all). Three knobs, in
`lfm::card_schedule`, each moving work and never a committed byte:

- LAMBDA_VM_GAP_PREP_SCOPE=1: `build_artifacts_counted` holds the card
  only around the build's device commits (`build_artifacts_sectioned`);
  the groups under the device floor are committed on the host first. With
  the card trace on, each build prints its host/device split.
- LAMBDA_VM_GAP_PREP_NICE=<1..19>: host-only phases run on a rayon pool of
  their own whose threads take that nice value (Linux setpriority; libc as
  a Linux-only dependency): `lfm_prepare`'s execute and fill, the sectioned
  build's host half, and the STARK tree's wrap reconstruct, emit, census and
  harvest and the global child's harvest, emits and host verifies. The card
  holder keeps the CPU and the global pool.
- LAMBDA_VM_GAP_PREP_AHEAD=1: a level-0 wrap builds its artifacts on a
  helper thread while it executes and fills (`lfm_prove` is now
  `lfm_prepare` + `lfm_prove_prepared`; nothing before multi_prove reads the
  artifacts). Costs host memory: traces exist while the build may queue.

The permit stays a mutual exclusion under all three, and a build's device
commits run in the windows they always did. Unset, every path is the old
one; the STARK driver prints a CARD SCHEDULE line only when a knob is set.

Tests: the sectioned build equals the whole build over four programs
(split hash, three BLAKE3 chunks) and three one-row modes, and enters its
section once exactly when it has device work; on cuda, every device commit
lands inside the section. Execute and fill on the pool are cell-identical
to inline over the trace-identity cases; the pool's threads carry the nice
value (Linux). The prepared prove publishes the same words and verifies
(box-scale), refuses another hasher's artifacts, and the driver's AHEAD
helper returns the plain build's artifacts and a verifying proof
(box-scale).

Each WHIR base-chain round ground 20 bits before three challenges. Only the
query grind buys proven bits as placed: the folding grind sits before the
round's first sumcheck message, so the first folding challenge is redrawn by
varying that message at one hash a try, and the out-of-domain grind follows
the out-of-domain point. The new ZF lever `whir_grind` therefore defaults to
`query`: GrindBits::query_only(20) under NonceLayout::Spent, one grind and
one nonce word a round, 518 grinds a block instead of 1,472 at stack 27. The
query count reads the query grind alone and stays 112. The proven bits per
phase do not move: chain minimum 130.393 at stack 27, pipeline minimum
128.946.

LAMBDA_VM_ZF_WHIR_GRIND=all is the opt-out: GrindBits::uniform(20) under
NonceLayout::Three, the production config from before this commit. A test
pins it against a literal, and its chain programs against the values printed
at 0428c39. The banner gains `whir_grind=`. No univariate option reads the
lever, so no STARK proof, program or id moves.

Re-blessed: the production default chain's pins now describe the P2 chain
(12 grind permutations, 16,411 permutations, 32,590 arena words,
150,258 / 202,873 rows). Its previous pins move unchanged to the opt-out's
test. The banner strings in zf_format's tests gain the new key.

…head of it

The first prove of a process builds every domain and twiddle set its tables
need inside its prepass (0.38 s of the STARK base's first PROVE SPLIT on the
G1 traced run, with the card idle), and each device NTT twiddle size and
staging pair at its first use, between two kernels. These entry points let a
caller build the same state beforehand, off the prove:

- `Domain::from_options`: `Domain::new` reads only the options from its AIR,
  so the same domain can be built before any AIR exists; `new` delegates.
- `prover::warm_domain_and_twiddles`: fills the process-wide cache entry that
  `domain_and_twiddles` looks up, through the same function, so a warmed
  prove reads exactly what it would have built.
- `gpu_lde::prewarm_device`, over `device::prewarm_twiddles` and
  `device::prewarm_staging_pairs`: the backend, every twiddle size up to a
  bound, and a number of staging pairs, built by the functions that build
  them on demand.

Nothing calls them yet; no value a prove commits or reads changes.

…VM_OOD_COLUMNS_ON_CALLER)

A round-3 OOD table is one or two rows high, and `Table::columns` transposes
it with a rayon parallel iterator. The per-table drivers of `multi_prove` are
plain OS threads, so each call is injected into the global pool and the driver
waits for a worker, with its table's next device work unsubmitted. When the
pool is busy with other work, that microsecond transpose waits behind it: on
the STARK base's G1 traced run the host-only OOD absorb summed 5.16 s over
split 9's tables and 2.73 s over split 11's, while the level-0 lead-in was
verifying base epochs in the base's tail, against about 0.02 s in a quiet
split. Three sites read these columns per table: the round-3 absorb and the
two device DEEP dispatches (and the host DEEP loop).

`LAMBDA_VM_OOD_COLUMNS_ON_CALLER=1` builds them with `Table::columns_serial`,
the same per-column read on the calling thread. Unset or `0` keeps the pool
(today's); anything else panics. The values and their order are those of
`Table::columns`, so the transcript and the proof are the same bytes.

Tests (`tests::host_schedule_tests`): the serial transpose equals the parallel
one; the switch's parsing; and a whole multi-table proof, grinding off, is
byte-identical with the switch on and off, with a counter showing the named
arm ran. Reversing the serial column order fails the byte test. The file also
tests the warm-up entry points of the previous commit: an options-built domain
equals the AIR-built one, and a warmed cache entry is the one a lookup hits.

…AD_AHEAD)

Before the card has anything to do, the serial head commits DECODE's
precomputed columns on the host (RPX over a 2^22-row LDE, about a second on
the block ELF, before epoch 0 executes), epoch 0's builder then initialises
the device, and the first prove's prepass builds every domain and twiddle
set. On the G1 traced run that is 2.44 s from run start to the first PROVE
SPLIT, plus 0.38 s of prepass, all with the card idle.

`LAMBDA_VM_BASE_HEAD_AHEAD=1` starts two helpers beside the producer: one
initialises the device, commits DECODE there and then builds the device's
per-size twiddles and four staging pairs; the other builds the host domains
and twiddles of every trace size up to the epoch's. The epochs wait for the
commitment where they first use it (each epoch's preparation, or its prove),
and the base's observer hears it from the helper, before any epoch is
prepared. Unset or `0` keeps the serial head (today's); anything else panics.
Each helper step prints a `BASE HEAD:` stamp under `LAMBDA_VM_BASE_SPLIT`.

The device commitment is `decode::compute_precomputed_commitment_device_or_host`:
DECODE's five precomputed columns, row-major, through
`lfm::commit::commit_group_device_or_host_with`, whose device root its device
tests pin to the host's; `multi_prove` also rebuilds DECODE's precomputed tree
at the first epoch and refuses the proof if its root differs. The host arm is
the same interpolate, coset-evaluate and commit as the serial head's.

Tests: the device-or-host root equals the host root in both leaf layouts, for
a 13- and a 4,097-instruction program (the latter crosses the device's commit
floor on a device build) and from an ELF; building the group column-major
fails both. The head run ahead proves what the serial head proves (the shared
comparison, now `assert_same_proved`, also used by the prep-ahead test), and
the observer hears the serial head's commitment exactly once. The switch's
parsing.

…TREE_TAIL_THREADS)

The level-0 lead-in builds wrap prologues in the base's tail: each verifies
its base epoch, fanning out over every thread of the global rayon pool while
the base still proves its last epochs. The base's per-table drivers are plain
OS threads, so each parallel iterator they start is injected into that same
pool and waits for a worker. On the STARK base's G1 traced run the prologue
spans hold 4.83 s of the base's 10.88 s of card idle, and the base's host-only
OOD absorb, one such injection, summed 5.16 s over split 9's tables against
about 0.02 s in a quiet split.

`LFM_TREE_TAIL_THREADS=<n>` runs each prologue inside a rayon pool of n
threads of its own, so it fans out over those and never queues ahead of the
base's work in the global pool. The helper takes the lead-in's context before
entering the pool, so no pool thread waits on the base. Unset, empty or `0`
keeps the global pool (today's); anything but a count panics. The prologues
compute the same programs and arenas either way; the tree's program ids are
the check on a box run.

Tests: the switch's parsing, and work run in a pool of its own fans out over
that pool's threads and returns what it computed.

`LAMBDA_VM_GPU_DEVICE_ONLY_THRESHOLD` decides which tables keep a host copy
of their LDEs, and those copies are downloaded inside each table's commit:
on the STARK base's G1 traced run, 39.74 GB of retained-LDE downloads (8.08 s
of driver time), about 80 % of it KECCAK_RND and ECDAS tables that sit below
the 2^19-row default only by row count. A run that moves the threshold has to
say so in its log, so the resolved envelope is printed once, where it is read:
`[gpu] device-only envelope: LDE >= <rows> rows (<source>)`. No behaviour
changes.

Two checks for a device build, so a host fallback cannot pass as the device:

- the head helper's device stamp says whether the device took the warm-up
  (`BASE HEAD: device warm-up` or `... declined`), since a decline is
  silent by design (the prove then builds the same state on demand);
- `the_head_decode_root_is_committed_on_the_device` (cuda): the 4,097-
  instruction DECODE map, 8,192 rows at blowup 2 and so above the device's
  commit floor, moves the device group counter and still gives the host
  root. The counter is process-wide, so the test is run on its own.

The ZfFormat::DEFAULT doc quoted a block timing for whir_grind=query from an
earlier measurement. A measured number in a comment goes stale, so the doc
now says what the lever does and why it loses no proven bits.

The same reasoning in whir_chain's module header, GrindBits::query_only and
WhirGrind gave the out-of-domain grind's reason as "it follows the
out-of-domain point". That is half of it: the grind sits right before the
batching challenge and does guard it. Dropping it costs nothing because the
batching challenge has far more bits than the target without any grind.

Comments only.

the_inner_node_verifies_two_leaf_nodes needs FAN_IN^2 = 4 epochs and took
FIXTURE_EPOCH_LOG2 - 1. Since 8f9aef1 moved the fixture to the 48-cycle
continuation-fixture at FIXTURE_EPOCH_LOG2 = 5, that is 16-cycle epochs and
three of them, so this box-tier test has stopped at its own epoch-count
assert in setup, before proving anything, under either wrap attestation. A
pre-existing fixture drift, found by the gates at e413989.

Two below the shared constant is safe by an assertion the suite already
holds: the_fixture_guest_commits_in_an_intermediate_epoch keeps the guest
above one shared epoch and within two, so 8-cycle epochs give at least five
(six today), where 16-cycle ones give three or four.

…le v2)

Job 202's NICE arms lost 9.65 s at STARK level 0 while their mechanism
moved the right way (level-0 held time -5.4 s). The cause was the one
host-phase pool shared by the six level-0 workers: every whole host
phase was an injected job there, and a rayon thread blocked in a join
runs injected jobs before it returns to its own (rayon-core 1.13
wait_until_cold). A thread waiting inside one wrap's reconstruct ran
other wraps' whole phases nested on its stack, so the reconstructs that
started first finished last (2-3 s became up to 22 s) and the card sat
with no holder for 17 s of the level.

host_phase now installs into a pool of the CALLING thread's own, built
at its first host phase and dropped with the thread. A worker runs one
phase at a time, so its pool only ever holds that phase's jobs; a
caller that is already a rayon worker runs the phase inline. Each pool
prints one line naming its caller and how many of its threads took the
nice value, counted after every thread has started. Knob unset: inline,
as before.

Tests: two callers' phases never share a thread (with the shared-pool
design as the control, which puts both on the same threads); a caller
reuses its own pool; a rayon worker runs a phase inline; unset runs on
the caller; a new pool reports every thread.

A table outside the device-only envelope downloads its whole main and aux
LDE inside its commit, on the driver that would otherwise submit its next
table. At the 2^19 default the STARK block's base downloaded 39.74 GB that
way (8.08 s of driver time), most of it KECCAK_RND and ECDAS tables of 1,480
and 521 columns whose device paths already run: they sat outside the envelope
by row count alone. At 2^16, with the barycentric floor (trace >= 2^14 rows)
below it, the base downloads 7.27 GB and the block proves 1.40 s faster
(FAST job 206, ds850-861, two arms each: wall -1.40 s, base -1.10 s; program
ids unchanged, the root verified).

`LAMBDA_VM_GPU_DEVICE_ONLY_THRESHOLD=524288` restores the 2^19 envelope. The
default is process-wide, so the WHIR pipeline's recursion proofs (FRI STARKs
through the same gate) take it too; that pipeline was not measured.

The head helpers (DECODE committed on the device, the first prove's domain,
twiddle and staging state built beside epoch 0) become the default:
`LAMBDA_VM_BASE_HEAD_AHEAD` unset, empty or `1` runs the head ahead, and `0`
is the named opt-out that runs the serial head as before. FAST job 206
(ds850-861, two arms each against the serial head): the head 2.4 -> 1.0 s, the
first prepass 0.37 -> 0.00 s, the base -2.00 s, the block -1.45 s; program ids
unchanged, the root verified.

The switch's test now pins the new reading (ahead unless exactly `0`); the
equivalence test still proves both heads by parameter.

… by default

The level-0 lead-in's prologues put parallel work on whatever pool they run
in while the base still proves its last epochs, and the base's per-table
drivers, plain OS threads, queue their own parallel iterators behind it in the
global pool: the host-only OOD absorb summed 5.2-5.3 s over split 9's tables
in all three G1 arms. In a pool of 16 threads of their own (FAST job 206,
ds850-861, two arms each against the global pool) the base's worst split
absorb fell to 0.04 s, the base by 2.35 s and the block by 2.20 s, level 0
+0.05 s; program ids unchanged.

The pool now belongs to each `LeadIn`, sized by its caller: the STARK tree
defaults to `STARK_TAIL_THREADS` (16); the WHIR tree keeps the global pool,
its tail not having been measured in one. `LFM_TREE_TAIL_THREADS` overrides
either (`0` is the global pool, the named opt-out; a count, a pool of that
size), and the line naming the choice is printed where the lead-in starts.
The rationale no longer says the prologues' verify fans out over the pool;
what is established is that isolating them removed the stalls.

Tests: the switch over each pipeline's default; a lead-in with a pool of 3
builds its prologues on that pool's threads and one without a pool does not
(routing the prologue around the pool fails it).

…ries

the_inner_node_verifies_two_leaf_nodes checked the composition property,
that a node's published schema does not change with its level, as
inner_layout.total() == leaf_layouts[0].total(). A node publishes its last
child's output halves (emit_node_publishes), so that compare also required
the FIRST leaf's carried output to be as long as the LAST leaf's: a fact
about which epoch committed, not about the level. It held while neither
leaf's last epoch committed. At the 8-cycle epochs the gate now runs at,
the fixture commits in epoch 1, the first leaf's last, so that leaf
publishes 146 words against the inner node's 144, under either STARK wrap
attestation.

Compare the words the two proofs published instead, the inner node against
the last leaf, whose output halves it carries. The compare of two layouts
built from the same count could not fail; the published counts can.

LFM_TREE_TAIL_THREADS now also takes `per-helper:<n>`: each lead-in helper
builds its prologues in a rayon pool of n threads of its own. The default
does not change (one shared pool of 16 for the STARK tree, the global pool
for the WHIR tree), and `0` is still the global pool.

Why: each helper installs a whole prologue, with joins inside, into its
pool. A pool thread waiting in a join also takes injected jobs, so in a
pool two helpers share it can run the other helper's whole prologue nested
on its stack and finish its own only after that one; F-PREP measured that
inversion on level 0. With one pool per helper, each pool has one caller
and the inversion cannot happen.

A per-helper pool of no threads is refused (rayon would read 0 as every
core). A test checks that two helpers building at once run on two pools,
each prologue on one pool of the per-helper width. Routing every helper to
the first pool fails it.

Conflict in prover/src/zf_format.rs resolved by keeping both defaults:
one_row=auto (the STARK pipeline's measured setting) and whir_grind=query
(P2-W, which changes no STARK proof). The default banner is now
cap=auto whir_cap=auto fri=dp one_row=auto whir_folds=first6 whir_stack=27 whir_grind=query.

…elper by default

The STARK tree's default for LFM_TREE_TAIL_THREADS is now one pool of 8
threads per helper, the same 16 threads the shared pool had.
LFM_TREE_TAIL_THREADS=16 is the named way back to one shared pool, and 0
is still the global pool. The WHIR tree keeps the global pool.

A pool per helper has one caller, so a pool thread waiting inside one
prologue can no longer run the other helper's whole prologue nested and
finish its own late. FAST job 2115 (ds884-887, S P P S, two arms each)
measured the per-helper pools against the shared pool:
- wall +0.30 s, base -0.20 s, level 0 +0.70 s;
- all inside the 0.8 s noise, and program ids unchanged.
The only prologue it slows is the lead-in's last, which runs alone:
5.4-5.5 s on 8 threads against 3.9-4.1 s on the shared 16.

…by default

STARK block ABBA: -4.15 s (EFFECTIVE). LAMBDA_VM_STARK_WRAP_FOLD=1 restores the
in-guest fold and today's program ids byte for byte. Also repairs the box-tier
inner-node test (a quarter-epoch fixture tree; the compare against the leaf it
carries), whose failure was pre-existing at 8934b59.

…ad-in

Head ahead (LAMBDA_VM_BASE_HEAD_AHEAD), the device-only envelope from LDE 2^16
(LAMBDA_VM_GPU_DEVICE_ONLY_THRESHOLD) and the tree's lead-in prologues in their
own pools, 8 threads per helper (LFM_TREE_TAIL_THREADS). STARK block ABBA:
-5.05 s (confirmed); per-helper pools NO EFFECT against one shared pool.

Both RPX implementations (prover lfm::rpo::Rpo256::mds, used by the block
path's RpxStarkHash, and crypto::hash::rpx::mds) built each output lane with
a core::array::from_fn closure. The closure's generic from_fn wrapper is
placed in a codegen unit of rustc's choosing and is inlined into mds only
when that unit happens to be mds's own. When it is not, every lane is an
out-of-line call that recomputes (j - i) mod 12 with a 64-bit multiply per
term: about a fifth more instructions per permutation.

That is the two-speed host verify on the STARK tree. A Linux x86-64 cross
build of the prover test crate at 8934b59, ef6d4be and 3fd644e shows
mds inlined (2499 B, no calls) only at ef6d4be, the one FAST build, and
twelve closure calls at the other two, the SLOW builds. Crypto's mds makes
the twelve calls in its current partitioning too.

Loops over a precomputed circulant compile the same way in every build. The
permutation's values are unchanged: the RPO and RPX known-answer vectors, the
two-implementation agreement test and a new test against the circulant
definition all pass.

… knobs

LAMBDA_VM_GAP_PREP_NICE now defaults to 10: the tree driver's reconstruct,
emit and harvest and every LFM prove's execute and fill run on a pool of the
calling thread's own, its threads at nice 10, so the proof holding the card
keeps the CPU. LAMBDA_VM_GAP_PREP_NICE=0 is the opt-out and restores the
schedule before the knob; 1..=19 picks another value.

Measured at bbdac70 on FAST (F-PREP job 224, ABBA, one binary): the STARK
tree took 1.55 s less (A 73.8 / 73.7 s, B 72.4 / 72.0 s). Level-0 card holds
shrank 4.15 s; the card waits 2.49 s longer for the next wrap's host work.
No wrap's reconstruct slowed past the stall guard (3.27 s against 6.26 s).

Proofs are unchanged: a host phase moves where execute and fill run, not what
they write (trace_identity_tests::execute_and_fill_on_the_host_phase_pool_are_byte_identical).
The lead-in's prologues are untouched: they run in F-SIDLE's per-helper pools
and never go through host_phase.